Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2229b077d6ebd2ff42d665fe1c32501df8915dff --onto a71f158f7bd96ff9ea846f7ff4cc658de3c8b0f9. You can force Mathlib CI using the force-mathlib-ci label. (2026-05-11 09:59:28)
• ✅ Mathlib branch lean-pr-testing-13700 has successfully built against this PR. (2026-05-11 20:52:47) View Log
• ✅ Mathlib branch lean-pr-testing-13700 has successfully built against this PR. (2026-05-11 23:12:40) View Log
• ✅ Mathlib branch lean-pr-testing-13700 has successfully built against this PR. (2026-05-12 23:57:12) View Log

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 2229b077d6ebd2ff42d665fe1c32501df8915dff --onto a71f158f7bd96ff9ea846f7ff4cc658de3c8b0f9. You can force reference manual CI using the force-manual-ci label. (2026-05-11 09:59:29)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-05-11 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-05-11 19:57:40)
• ✅ Reference manual branch lean-pr-testing-13700 has successfully built against this PR. (2026-05-12 23:09:44) View Log
• 🟡 Reference manual branch lean-pr-testing-13700 build against this PR didn't complete normally. (2026-05-12 23:11:36) View Log

!bench

Benchmark results for 5d63f74 against 2229b07 are in. There are significant results. @hargoniX

• 🟥 build exited with code 1
• 🟥 other exited with code 1

No significant changes detected.

!bench

Benchmark results for 9df0343 against 2229b07 are in. There are significant results. @hargoniX

• 🟥 build exited with code 1
• 🟥 other exited with code 1

No significant changes detected.

!bench

Benchmark results for f6f7db2 against 2229b07 are in. There are significant results. @hargoniX

• 🟥 build exited with code 1
• 🟥 other exited with code 1

No significant changes detected.

!bench

Benchmark results for c5f8dc8 against 2229b07 are in. There are significant results. @hargoniX

• 🟥 build exited with code 1

Large changes (7✅, 10🟥)

• 🟥 compiled/ilean_roundtrip//instructions: +138.7M (+0.59%)
• ✅ compiled/nat_repr//instructions: -548.5M (-1.39%)
• 🟥 compiled/phashmap//instructions: +71.7M (+0.81%)
• 🟥 lake/inundation/build clean//instructions: +213.2G (+13.71%)
• 🟥 lake/inundation/build clean//wall-clock: +2s (+7.80%)
• 🟥 lake/inundation/config elab//instructions: +69.8M (+2.89%)
• 🟥 lake/inundation/config import//instructions: +70.6M (+5.82%)
• 🟥 lake/inundation/config tree//instructions: +70.2M (+5.63%)
• 🟥 lake/inundation/env//instructions: +72.1M (+5.84%)
• 🟥 lake/inundation/startup//instructions: +66.7M (+34.75%)
• 🟥 misc/import Lean//instructions: +72.0M (+4.82%)
• ✅ misc/re-elab Init.Data.BitVec.Lemmas//task-clock: -21s (-24.29%)
• ✅ misc/re-elab Init.Data.BitVec.Lemmas//wall-clock: -4s (-17.41%)
• ✅ misc/re-elab watchdog Init.Data.List.Sublist//instructions: -318.1G (-65.14%)
• ✅ misc/re-elab watchdog Init.Data.List.Sublist//task-clock: -40s (-64.10%)
• ✅ misc/re-elab watchdog Init.Data.List.Sublist//wall-clock: -15s (-69.21%)
• ✅ size/compile/.out//bytes: -23MiB (-1.16%)

Medium changes (3✅, 18🟥)

Too many entries to display here. View the full report on radar instead.

Small changes (4✅, 20🟥)

Too many entries to display here. View the full report on radar instead.

!bench

Benchmarking d129997 against 2229b07 (preliminary results).

_{React with 👀 to be notified when the results are in. The command author is always notified.}